Orbit Map & Orbit-Stabilizer Theorem: The fundamental bijection
The orbit-stabilizer theorem establishes a fundamental bijection between the quotient G/Stab(x) (left cosets of the stabilizer) and Orb(x) (the orbit of x). This bijection proves that |G| = |Orb(x)| · |Stab(x)|, one of the most important identities in group theory. The proof constructs an explicit map from cosets to orbit elements, shows it's well-defined (independent of coset representative), then proves it's both injective and surjective. This theorem is the foundation for Burnside's Lemma and countless applications in algebra, combinatorics, and geometry.
Interactive Lean 4 proof — click a line to see its strategy and explanation inline
Strategy: Define the orbit map's type signature — from cosets of the stabilizer to the orbit.
Explanation: We're constructing a function from G ⧸ Stab(x) (the quotient group, whose elements are left cosets g·Stab(x)) to Orb(x) (the set {g·x | g ∈ G}). This map will send each coset ⟦g⟧ to the orbit element g·x. The key challenge is proving this is well-defined: if ⟦a⟧ = ⟦b⟧ (same coset), we must show a·x = b·x. This signature sets up the fundamental bijection of the orbit-stabilizer theorem.
Strategy: Use Quotient.lift to define a function on the quotient by providing a function on representatives.
Explanation: Quotient.lift is the standard way to define functions out of quotient types. We provide: (1) A function g ↦ A.act g x on representatives (raw group elements), which produces an element of Orb(x). The angle brackets ⟨A.act g x, ⟨g, rfl⟩⟩ package the orbit element: the first component is g·x, the second is the proof that g·x ∈ Orb(x) (witnessed by g itself, with rfl proving g·x = g·x). (2) A proof (the by block) that this function respects the equivalence relation: if a ≈ b (same coset), then a·x = b·x. This well-definedness proof is crucial.
Strategy: Introduce the two representatives a and b and the hypothesis that they're equivalent (same coset).
Explanation: We need to prove: if a ≈ b (i.e., ⟦a⟧ = ⟦b⟧ as cosets), then our function gives the same result. The intro tactic brings in arbitrary group elements a, b and the hypothesis hab : a ≈ b. In the quotient group G ⧸ Stab(x), the relation ≈ is defined by: a ≈ b iff a⁻¹·b ∈ Stab(x) iff (a⁻¹·b)·x = x. Our goal is to show A.act a x = A.act b x.
Strategy: Simplify the goal to strip away the subtype packaging.
Explanation: Our goal is ⟨A.act a x, ...⟩ = ⟨A.act b x, ...⟩ where these are subtypes (elements of Orb(x) with their membership proofs). Subtype.mk.injEq states that two subtype values are equal iff their underlying values are equal (the proofs are irrelevant by proof irrelevance). This simplifies the goal to just A.act a x = A.act b x, stripping away the membership proof components.
Strategy: Use Quotient.sound to convert the equivalence relation into an equality of quotient elements.
Explanation: Quotient.sound is the fundamental lemma for quotients: if a ≈ b (as an equivalence relation), then ⟦a⟧ = ⟦b⟧ (as quotient elements). We apply it to hab : a ≈ b to get q_eq : QuotientGroup.mk a = QuotientGroup.mk b. This converts from the abstract relation (which might be defined in various ways) to a concrete equality statement in the quotient type. This equality is what we'll unpack to extract information about the stabilizer.
Strategy: Rewrite the quotient equality using the characterization of coset equality.
Explanation: QuotientGroup.eq is the key lemma: ⟦a⟧ = ⟦b⟧ in G/H iff a⁻¹·b ∈ H. For our quotient G ⧸ Stab(x), this becomes: ⟦a⟧ = ⟦b⟧ iff a⁻¹·b ∈ Stab(x). We rewrite q_eq using this lemma, transforming it from an equality in the quotient type to a membership statement in the stabilizer. Now q_eq states exactly what we need: a⁻¹·b is in the stabilizer of x.
Strategy: Extract the concrete meaning of stabilizer membership: the element fixes x.
Explanation: By definition, g ∈ Stab(x) means A.act g x = x. Since q_eq now states a⁻¹·b ∈ Stab(x), we can extract the defining property: A.act (a⁻¹·b) x = x. We name this h_stab — this is the key fact we'll use to show a·x = b·x. The element a⁻¹·b fixes x, which geometrically means a and b send x to the same place in the orbit.
Strategy: Use equational reasoning to show a·x = b·x by inserting the fixing element.
Explanation: This calc chain is the heart of the well-definedness proof:
• Start with A.act a x (what we want to show equals A.act b x).
• Step 1: Replace x with A.act (a⁻¹·b) x using h_stab (since (a⁻¹·b)·x = x, we can substitute).
• Step 2: Use mul_act backwards to combine the two actions: a·((a⁻¹·b)·x) = (a·(a⁻¹·b))·x.
• Step 3: Simplify the group multiplication: a·(a⁻¹·b) = (a·a⁻¹)·b = 1·b = b, so we get b·x.
This completes the proof that a·x = b·x, establishing well-definedness. The orbit map is now properly defined! □
💡 Tip: Click on any line above to see its strategy and explanation inline. Click again to hide it.
Proving the orbit map is a bijection — both injective and surjective
Strategy: State the theorem — orbit_map is a bijection.
Explanation: We claim that orbit_map A x : G ⧸ Stab(x) → Orb(x) is bijective, meaning it's both injective (one-to-one) and surjective (onto). Function.Bijective is defined as the conjunction Injective ∧ Surjective, so we'll need to prove both properties. This bijection is the heart of the orbit-stabilizer theorem: it establishes a perfect correspondence between cosets and orbit elements, which immediately implies |G/Stab(x)| = |Orb(x)|, and by Lagrange's theorem, |G|/|Stab(x)| = |Orb(x)|.
Strategy: Split the bijection proof into injectivity and surjectivity.
Explanation: Since Function.Bijective is defined as a conjunction (Injective f ∧ Surjective f), the constructor tactic splits the goal into two subgoals: (1) prove orbit_map is injective, (2) prove orbit_map is surjective. We'll tackle injectivity first (if the map sends two cosets to the same orbit element, they must be the same coset), then surjectivity (every orbit element is hit by some coset).
Strategy: Begin the injectivity proof by introducing two quotient elements and the hypothesis that they map to the same orbit element.
Explanation: To prove injectivity, we assume orbit_map(qa) = orbit_map(qb) for quotient elements qa, qb ∈ G/Stab(x), and must show qa = qb. The intro tactic brings in qa, qb (arbitrary cosets) and h_eq : orbit_map A x qa = orbit_map A x qb. But qa and qb are wrapped in the quotient type — we need to unwrap them to work with actual group elements.
Strategy: Revert qa and qb back into the goal to prepare for quotient induction.
Explanation: We use revert to move qa and qb from the context back into the goal, changing the goal from "qa = qb" to "∀ qa qb, orbit_map qa = orbit_map qb → qa = qb". This is necessary because Quotient.inductionOn₂ (which we'll apply next) expects a goal that's universally quantified over two quotient elements. Revert is the opposite of intro — it generalizes specific variables back to quantified ones.
Strategy: Re-introduce qa and qb in preparation for induction.
Explanation: We immediately intro them back — this seems redundant, but it sets up the proper structure for Quotient.inductionOn₂. The goal is now structured as "∀ qa qb, P(qa, qb)" where we can apply quotient induction. This is a common pattern when working with quotient types: revert to generalize, then intro to get the right shape for induction.
Strategy: Apply quotient induction to unwrap both quotient elements simultaneously.
Explanation: Quotient.inductionOn₂ is the key tactic for working with quotients. It says: to prove a property P(qa, qb) for all quotient elements qa, qb, it suffices to prove P(⟦a⟧, ⟦b⟧) for all representatives a, b. After this tactic, qa and qb will be replaced by ⟦a⟧ and ⟦b⟧ where a and b are ordinary group elements. This "lifts" the proof from the abstract quotient level to the concrete element level, where we can use group operations directly. The ?_ placeholder says "I'll prove the resulting goal next".
Strategy: Introduce the unwrapped representatives a and b and the equality hypothesis.
Explanation: After induction, we're now working with concrete group elements a, b : G (not quotient elements). The goal is now: if orbit_map(⟦a⟧) = orbit_map(⟦b⟧), then ⟦a⟧ = ⟦b⟧. The hypothesis h_eq will be orbit_map A x ⟦a⟧ = orbit_map A x ⟦b⟧, which by definition of orbit_map simplifies to a·x = b·x (the two representatives send x to the same place). Our goal ⟦a⟧ = ⟦b⟧ means the cosets are equal.
Strategy: Simplify the hypothesis to extract the concrete equality.
Explanation: We simplify h_eq using:
• orbit_map: unfold the definition of orbit_map.
• Quotient.lift_mk: when you apply Quotient.lift to ⟦a⟧, it evaluates to the function applied to a directly.
• Subtype.ext_iff: two subtype elements are equal iff their underlying values are equal.
After these simplifications, h_eq becomes simply: A.act a x = A.act b x. This is the concrete fact we'll use to prove the cosets are equal.
Strategy: Apply the characterization of quotient equality in the reverse direction.
Explanation: QuotientGroup.eq states: ⟦a⟧ = ⟦b⟧ ↔ a⁻¹·b ∈ Stab(x). The .mpr ("modus ponens reverse") applies the right-to-left direction: to prove ⟦a⟧ = ⟦b⟧, it suffices to prove a⁻¹·b ∈ Stab(x). This changes our goal from a quotient equality to a group membership statement. Now we need to show a⁻¹·b ∈ Stab(x), which by definition means (a⁻¹·b)·x = x.
Strategy: Make the goal explicit — we need to show (a⁻¹·b) fixes x.
Explanation: The change tactic replaces the goal with a definitionally equal one, making it clearer. After applying QuotientGroup.eq.mpr, the goal is expressed in terms of the stabilizer membership predicate, which might be abstracted. We make it concrete: a⁻¹·b ∈ Stab(x) means by definition A.act (a⁻¹·b) x = x. This is the explicit form we'll prove using our hypothesis h_eq : a·x = b·x.
Strategy: Use equational reasoning to show (a⁻¹·b)·x = x from the hypothesis a·x = b·x.
Explanation: This calc chain is the mirror image of the orbit_map well-definedness proof:
• Start with A.act (a⁻¹·b) x.
• Step 1: Expand using mul_act: (a⁻¹·b)·x = a⁻¹·(b·x).
• Step 2: Use h_eq : a·x = b·x backwards to replace b·x with a·x: a⁻¹·(b·x) = a⁻¹·(a·x).
• Step 3: Combine using mul_act backwards: a⁻¹·(a·x) = (a⁻¹·a)·x.
• Step 4: Simplify group multiplication: a⁻¹·a = 1, so (a⁻¹·a)·x = 1·x.
• Step 5: Identity acts as identity: 1·x = x.
This proves (a⁻¹·b)·x = x, so a⁻¹·b ∈ Stab(x), so ⟦a⟧ = ⟦b⟧. Injectivity is complete! □
Strategy: Begin the surjectivity proof by introducing an arbitrary orbit element.
Explanation: To prove surjectivity, we must show: for every element in Orb(x), there exists a coset in G/Stab(x) that maps to it. The intro with pattern-matching ⟨y, hy⟩ unpacks an arbitrary element of orbit A x: y is the underlying element of X, and hy is the proof that y ∈ Orb(x). Our goal is now to produce some quotient element ⟦g⟧ ∈ G/Stab(x) such that orbit_map(⟦g⟧) = ⟨y, hy⟩.
Strategy: Extract the witness from the orbit membership proof.
Explanation: Since y ∈ Orb(x), by definition there exists some g ∈ G such that g·x = y. The hypothesis hy is exactly this existential proof. The obtain tactic (also called rcases or cases) extracts the witness g and the proof. The rfl pattern says "the proof is that y = g·x definitionally" — after obtain, y is replaced everywhere by A.act g x (it's not just equal, it IS g·x by definition). This is crucial: we don't just know y = g·x, we know y is literally g·x, so we can work with g·x directly.
Strategy: Provide the preimage — the coset of g.
Explanation: To prove surjectivity (∃ q, orbit_map q = y), we must provide a witness. The use tactic supplies ⟦g⟧ (the coset of g) as this witness. Now we need to prove that orbit_map(⟦g⟧) = ⟨A.act g x, ...⟩. But by definition, orbit_map(⟦g⟧) sends ⟦g⟧ to ⟨A.act g x, ⟨g, rfl⟩⟩, which is exactly the form we need. This should close the goal automatically.
Strategy: The goal is true by reflexivity — the definitions unfold to identical terms.
Explanation: After providing ⟦g⟧ as the witness, the goal becomes: orbit_map A x ⟦g⟧ = ⟨A.act g x, ...⟩. By definition, orbit_map A x ⟦g⟧ evaluates to exactly ⟨A.act g x, ⟨g, rfl⟩⟩. The two sides are definitionally equal (they're literally the same term after unfolding definitions), so rfl (reflexivity) proves it. Surjectivity is complete! □
Conclusion: We've proved both injectivity and surjectivity, so orbit_map is bijective. This establishes the orbit-stabilizer theorem: there's a perfect correspondence between G/Stab(x) and Orb(x). Taking cardinalities: |G/Stab(x)| = |Orb(x)|, and by Lagrange's theorem |G/Stab(x)| = |G|/|Stab(x)|, we get the classical identity |G| = |Orb(x)| · |Stab(x)|. ∎
💡 Tip: Click on any line above to see its strategy and explanation inline. Click again to hide it.
The orbit-stabilizer theorem proof has two main components:
Key insight: The orbit and stabilizer are dual views of the same symmetry. The orbit describes "where can x go?" (the equivalence class of x under the action), while the stabilizer describes "what fixes x?" (the subgroup preserving x). The bijection G/Stab(x) ≅ Orb(x) shows these are two sides of the same coin: each coset corresponds to exactly one orbit element, and the coset structure encodes the symmetry. This fundamental correspondence drives all of orbit-counting theory.
The fundamental way to define functions out of quotient types. To define f : Quotient R → Y, provide: (1) a function g : X → Y on representatives, and (2) a proof that if x ≈ x' then g(x) = g(x'). This ensures the function is well-defined (independent of which representative you choose). Without well-definedness, the function wouldn't make sense on the quotient.
The characterization of equality in quotient groups: ⟦a⟧ = ⟦b⟧ in G/H iff a⁻¹·b ∈ H. This bidirectional equivalence is the workhorse of quotient group reasoning. The forward direction (Quotient.sound) converts abstract equivalence to concrete membership. The reverse direction (.mpr) is used to prove coset equality by proving stabilizer membership. Essential for both well-definedness and injectivity.
Quotient induction principle for two variables: to prove ∀ qa qb : Quotient R, P(qa, qb), it suffices to prove ∀ a b : X, P(⟦a⟧, ⟦b⟧) for representatives. This "lifts" proofs from the concrete level (where you can use the underlying structure) to the quotient level (where you work with equivalence classes). Critical for proving properties about orbit_map since the domain is a quotient type.
The defining properties of group actions: (1) mul_act: (g·h)·x = g·(h·x) (actions compose correctly), and (2) one_act: 1·x = x (identity acts as identity). These axioms are used in every calc chain to manipulate action expressions. mul_act allows us to split or combine actions, while one_act provides the base case for simplification. These are the "rewrite rules" that make group action calculations work.
The orbit-stabilizer theorem is one of the most fundamental results in group theory, with far-reaching consequences. It establishes the equation |G| = |Orb(x)| · |Stab(x)|, which has profound implications:
Counting orbits: It's the foundation for Burnside's Lemma and Pólya enumeration theory, enabling us to count distinct configurations under symmetry.
Lagrange's theorem: When X = G with left multiplication action, Orb(x) = G and Stab(x) = {1}, recovering |G| = |G| · 1. For general subgroups H ≤ G, the action of G on G/H by left multiplication gives |G| = |G/H| · |H|, which is Lagrange's theorem.
Representation theory: The orbit-stabilizer theorem underlies the decomposition of representations into isotypic components, connecting representation theory and character theory.
Geometry and physics: In differential geometry and physics, orbits represent symmetry classes (e.g., energy levels, particle types), while stabilizers represent residual symmetries (isotropy groups). The theorem quantifies how symmetry breaking works.
The bijection G/Stab(x) ≅ Orb(x) is not just a cardinality statement — it's a natural isomorphism of G-sets, preserving all the group action structure. This makes it a cornerstone of equivariant mathematics.